<!DOCTYPE html>
<html class="client-nojs vector-feature-night-mode-disabled vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-sticky-header-enabled" lang="en" dir="ltr"><head>
<meta charset="UTF-8">
<title>Program analysis</title>
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<link rel="canonical" href="https://en.wikipedia.org/wiki/Program_analysis"> <link href="./mw/ext.cite.styles.css" rel="stylesheet" type="text/css">
<link href="./mw/skins.vector.icons.css" rel="stylesheet" type="text/css">
<link href="./mw/skins.vector.search.codex.styles.css" rel="stylesheet" type="text/css">
<link href="./mw/skins.vector.styles.css" rel="stylesheet" type="text/css">
<link href="./mw/user.styles.css" rel="stylesheet" type="text/css">
<meta name="ResourceLoaderDynamicStyles" content="">
<link rel="stylesheet" type="text/css" href="./mw/site.styles.css">
<link rel="stylesheet" type="text/css" href="./mw/noscript.css">
<link rel="stylesheet" type="text/css" href="./footer.css">
<link rel="stylesheet" type="text/css" href="./vector-2022.css">
</head>
<body class="skin--responsive skin-vector skin-vector-search-vue mediawiki ltr sitedir-ltr mw-hide-empty-elt ns-0 ns-subject page-Program_analysis rootpage-Program_analysis skin-vector-2022 action-view">
<div class="mw-page-container">
<div class="mw-page-container-inner">
<div class="mw-content-container">
<main id="content" class="mw-body">
<header class="mw-body-header vector-page-titlebar">
<h1 id="firstHeading" class="firstHeading mw-first-heading">
<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Program analysis</span></span>
</h1>
</header>
<a id="top"></a>
<div id="bodyContent" class="vector-body ve-init-mw-desktopArticleTarget-targetContainer" aria-labelledby="firstHeading" data-mw-ve-target-container="">
<div id="mw-content-text" class="mw-body-content mw-content-ltr" lang="en" dir="ltr"><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr">
<style data-mw-deduplicate="TemplateStyles:r1236090951">
/* start https://en.wikipedia.org/ */
.mw-parser-output .hatnote{font-style:italic}.mw-parser-output div.hatnote{padding-left:1.6em;margin-bottom:0.5em}.mw-parser-output .hatnote i{font-style:normal}.mw-parser-output .hatnote+link+.hatnote{margin-top:-0.5em}@media print{body.ns-0 .mw-parser-output .hatnote{display:none!important}}
/* end https://en.wikipedia.org/ */
</style><div role="note" class="hatnote navigation-not-searchable">For other uses, see <a href="Program_analysis_(disambiguation)" class="mw-disambig" title="Program analysis (disambiguation)">Program analysis (disambiguation)</a>.</div>
<style data-mw-deduplicate="TemplateStyles:r1305433154">
/* start https://en.wikipedia.org/ */
.mw-parser-output .ambox{border:1px solid #a2a9b1;border-left:10px solid #36c;background-color:#fbfbfb;box-sizing:border-box}.mw-parser-output .ambox+link+.ambox,.mw-parser-output .ambox+link+style+.ambox,.mw-parser-output .ambox+link+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+style+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+link+.ambox{margin-top:-1px}html body.mediawiki .mw-parser-output .ambox.mbox-small-left{margin:4px 1em 4px 0;overflow:hidden;width:238px;border-collapse:collapse;font-size:88%;line-height:1.25em}.mw-parser-output .ambox-speedy{border-left:10px solid #b32424;background-color:#fee7e6}.mw-parser-output .ambox-delete{border-left:10px solid #b32424}.mw-parser-output .ambox-content{border-left:10px solid #f28500}.mw-parser-output .ambox-style{border-left:10px solid #fc3}.mw-parser-output .ambox-move{border-left:10px solid #9932cc}.mw-parser-output .ambox-protection{border-left:10px solid #a2a9b1}.mw-parser-output .ambox .mbox-text{border:none;padding:0.25em 0.5em;width:100%}.mw-parser-output .ambox .mbox-image{border:none;padding:2px 0 2px 0.5em;text-align:center}.mw-parser-output .ambox .mbox-imageright{border:none;padding:2px 0.5em 2px 0;text-align:center}.mw-parser-output .ambox .mbox-empty-cell{border:none;padding:0;width:1px}.mw-parser-output .ambox .mbox-image-div{width:52px}@media(min-width:720px){.mw-parser-output .ambox{margin:0 10%}}@media print{body.ns-0 .mw-parser-output .ambox{display:none!important}}
/* end https://en.wikipedia.org/ */
</style>
<style data-mw-deduplicate="TemplateStyles:r1129693374">
/* start https://en.wikipedia.org/ */
.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}
/* end https://en.wikipedia.org/ */
</style><style data-mw-deduplicate="TemplateStyles:r1246091330">
/* start https://en.wikipedia.org/ */
.mw-parser-output .sidebar{width:22em;float:right;clear:right;margin:0.5em 0 1em 1em;background:var(--background-color-neutral-subtle,#f8f9fa);border:1px solid var(--border-color-base,#a2a9b1);padding:0.2em;text-align:center;line-height:1.4em;font-size:88%;border-collapse:collapse;display:table}body.skin-minerva .mw-parser-output .sidebar{display:table!important;float:right!important;margin:0.5em 0 1em 1em!important}.mw-parser-output .sidebar-subgroup{width:100%;margin:0;border-spacing:0}.mw-parser-output .sidebar-left{float:left;clear:left;margin:0.5em 1em 1em 0}.mw-parser-output .sidebar-none{float:none;clear:both;margin:0.5em 1em 1em 0}.mw-parser-output .sidebar-outer-title{padding:0 0.4em 0.2em;font-size:125%;line-height:1.2em;font-weight:bold}.mw-parser-output .sidebar-top-image{padding:0.4em}.mw-parser-output .sidebar-top-caption,.mw-parser-output .sidebar-pretitle-with-top-image,.mw-parser-output .sidebar-caption{padding:0.2em 0.4em 0;line-height:1.2em}.mw-parser-output .sidebar-pretitle{padding:0.4em 0.4em 0;line-height:1.2em}.mw-parser-output .sidebar-title,.mw-parser-output .sidebar-title-with-pretitle{padding:0.2em 0.8em;font-size:145%;line-height:1.2em}.mw-parser-output .sidebar-title-with-pretitle{padding:0.1em 0.4em}.mw-parser-output .sidebar-image{padding:0.2em 0.4em 0.4em}.mw-parser-output .sidebar-heading{padding:0.1em 0.4em}.mw-parser-output .sidebar-content{padding:0 0.5em 0.4em}.mw-parser-output .sidebar-content-with-subgroup{padding:0.1em 0.4em 0.2em}.mw-parser-output .sidebar-above,.mw-parser-output .sidebar-below{padding:0.3em 0.8em;font-weight:bold}.mw-parser-output .sidebar-collapse .sidebar-above,.mw-parser-output .sidebar-collapse .sidebar-below{border-top:1px solid #aaa;border-bottom:1px solid #aaa}.mw-parser-output .sidebar-navbar{text-align:right;font-size:115%;padding:0 0.4em 0.4em}.mw-parser-output .sidebar-list-title{padding:0 0.4em;text-align:left;font-weight:bold;line-height:1.6em;font-size:105%}.mw-parser-output .sidebar-list-title-c{padding:0 0.4em;text-align:center;margin:0 3.3em}@media(max-width:640px){body.mediawiki .mw-parser-output .sidebar{width:100%!important;clear:both;float:none!important;margin-left:0!important;margin-right:0!important}}body.skin--responsive .mw-parser-output .sidebar a>img{max-width:none!important}@media screen{html.skin-theme-clientpref-night .mw-parser-output .sidebar:not(.notheme) .sidebar-list-title,html.skin-theme-clientpref-night .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle{background:transparent!important}html.skin-theme-clientpref-night .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle a{color:var(--color-progressive)!important}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .sidebar:not(.notheme) .sidebar-list-title,html.skin-theme-clientpref-os .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle{background:transparent!important}html.skin-theme-clientpref-os .mw-parser-output .sidebar:not(.notheme) .sidebar-title-with-pretitle a{color:var(--color-progressive)!important}}@media print{body.ns-0 .mw-parser-output .sidebar{display:none!important}}
/* end https://en.wikipedia.org/ */
</style><table class="sidebar sidebar-collapse nomobile"><tbody><tr><td class="sidebar-pretitle">Part of a series on</td></tr><tr><th class="sidebar-title-with-pretitle"><a href="Software_development" title="Software development">Software development</a></th></tr><tr><td class="sidebar-content">
<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="color: var(--color-base)">Core activities</div><div class="sidebar-list-content mw-collapsible-content hlist">
<ul><li><a href="Data_modeling" title="Data modeling">Data modeling</a></li>
<li><a href="Software_development_process" title="Software development process">Processes</a></li>
<li><a href="Requirements_analysis" title="Requirements analysis">Requirements</a></li>
<li><a href="Software_design" title="Software design">Design</a></li>
<li><a href="Software_construction" title="Software construction">Construction</a></li>
<li><a href="Software_engineering" title="Software engineering">Engineering</a></li>
<li><a href="Software_testing" title="Software testing">Testing</a></li>
<li><a href="Debugging" title="Debugging">Debugging</a></li>
<li><a href="Software_deployment" title="Software deployment">Deployment</a></li>
<li><a href="Software_maintenance" title="Software maintenance">Maintenance</a></li></ul></div></div></td>
</tr><tr><td class="sidebar-content">
<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="color: var(--color-base)">Paradigms and models</div><div class="sidebar-list-content mw-collapsible-content hlist">
<ul><li><a href="Agile_software_development" title="Agile software development">Agile</a></li>
<li><a href="Cleanroom_software_engineering" title="Cleanroom software engineering">Cleanroom</a></li>
<li><a href="Incremental_build_model" title="Incremental build model">Incremental</a></li>
<li><a href="Software_prototyping" title="Software prototyping">Prototyping</a></li>
<li><a href="Spiral_model" title="Spiral model">Spiral</a></li>
<li><a href="V-model_(software_development)" title="V-model (software development)">V model</a></li>
<li><a href="Waterfall_model" title="Waterfall model">Waterfall</a></li></ul></div></div></td>
</tr><tr><td class="sidebar-content">
<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="color: var(--color-base)"><a href="Software_development_methodology" class="mw-redirect" title="Software development methodology">Methodologies</a> and frameworks</div><div class="sidebar-list-content mw-collapsible-content hlist">
<ul><li><a href="Adaptive_software_development" title="Adaptive software development">ASD</a></li>
<li><a href="Disciplined_agile_delivery" title="Disciplined agile delivery">DAD</a></li>
<li><a href="DevOps" title="DevOps">DevOps</a></li>
<li><a href="Dynamic_systems_development_method" title="Dynamic systems development method">DSDM</a></li>
<li><a href="Feature-driven_development" title="Feature-driven development">FDD</a></li>
<li><a href="Iterative_and_incremental_development" title="Iterative and incremental development">IID</a></li>
<li><a href="Kanban_(development)" title="Kanban (development)">Kanban</a></li>
<li><a href="Lean_software_development" title="Lean software development">Lean SD</a></li>
<li><a href="Scrum_(software_development)#Large-scale_Scrum" title="Scrum (software development)">LeSS</a></li>
<li><a href="Model-driven_development" class="mw-redirect" title="Model-driven development">MDD</a></li>
<li><a href="Microsoft_Solutions_Framework" title="Microsoft Solutions Framework">MSF</a></li>
<li><a href="Personal_software_process" title="Personal software process">PSP</a></li>
<li><a href="Rapid_application_development" title="Rapid application development">RAD</a></li>
<li><a href="Rational_unified_process" title="Rational unified process">RUP</a></li>
<li><a href="Scaled_agile_framework" title="Scaled agile framework">SAFe</a></li>
<li><a href="Scrum_(software_development)" title="Scrum (software development)">Scrum</a></li>
<li><a href="SEMAT" title="SEMAT">SEMAT</a></li>
<li><a href="Test-driven_development" title="Test-driven development">TDD</a></li>
<li><a href="Team_software_process" title="Team software process">TSP</a></li>
<li><a href="Unified_process" title="Unified process">UP</a></li>
<li><a href="Extreme_programming" title="Extreme programming">XP</a></li></ul></div></div></td>
</tr><tr><td class="sidebar-content">
<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="color: var(--color-base)">Supporting disciplines</div><div class="sidebar-list-content mw-collapsible-content hlist">
<ul><li><a href="Software_configuration_management" title="Software configuration management">Configuration management</a></li>
<li><a href="Deployment_management#Computer_science" title="Deployment management">Deployment management</a></li>
<li><a href="Software_documentation" title="Software documentation">Documentation</a></li>
<li><a href="Software_project_management" title="Software project management">Project management</a></li>
<li><a href="Software_quality_assurance" title="Software quality assurance">Quality assurance</a></li>
<li><a href="User_experience" title="User experience">User experience</a></li></ul></div></div></td>
</tr><tr><td class="sidebar-content">
<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="color: var(--color-base)">Practices</div><div class="sidebar-list-content mw-collapsible-content hlist">
<ul><li><a href="Acceptance_test-driven_development" title="Acceptance test-driven development">ATDD</a></li>
<li><a href="Behavior-driven_development" title="Behavior-driven development">BDD</a></li>
<li><a href="Extreme_programming_practices#Collective_code_ownership" title="Extreme programming practices">CCO</a></li>
<li><a href="Continuous_delivery" title="Continuous delivery">CD</a></li>
<li><a href="Continuous_integration" title="Continuous integration">CI</a></li>
<li><a href="Domain-driven_design" title="Domain-driven design">DDD</a></li>
<li><a href="Pair_programming" title="Pair programming">PP</a></li>
<li><a href="Specification_by_example" title="Specification by example">SBE</a></li>
<li><a href="Stand-up_meeting" title="Stand-up meeting">Stand-up</a></li>
<li><a href="Test-driven_development" title="Test-driven development">TDD</a></li></ul></div></div></td>
</tr><tr><td class="sidebar-content">
<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="color: var(--color-base)"><a href="Programming_tool" title="Programming tool">Tools</a></div><div class="sidebar-list-content mw-collapsible-content hlist">
<ul><li><a href="Build_automation" title="Build automation">Build automation</a></li>
<li><a href="Compiler" title="Compiler">Compiler</a></li>
<li><a href="Debugger" title="Debugger">Debugger</a></li>
<li><a href="Graphical_user_interface_builder" title="Graphical user interface builder">GUI builder</a></li>
<li><a href="Integrated_development_environment" title="Integrated development environment">IDE</a></li>
<li><a href="Infrastructure_as_code" title="Infrastructure as code">Infrastructure as code</a></li>
<li><a href="Profiling_(computer_programming)" title="Profiling (computer programming)">Profiler</a></li>
<li><a href="Application-release_automation" title="Application-release automation">Release automation</a></li>
<li><a href="UML_tool" title="UML tool">UML Modeling</a></li></ul></div></div></td>
</tr><tr><td class="sidebar-content">
<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="color: var(--color-base)">Standards and bodies of knowledge</div><div class="sidebar-list-content mw-collapsible-content hlist">
<ul><li><a href="Capability_Maturity_Model_Integration" title="Capability Maturity Model Integration">CMMI</a></li>
<li><a href="IEEE_Standards_Association" title="IEEE Standards Association">IEEE standards</a></li>
<li><a href="International_Requirements_Engineering_Board" title="International Requirements Engineering Board">IREB</a></li>
<li><a href="ISO_9001" class="mw-redirect" title="ISO 9001">ISO 9001</a></li>
<li><a href="ISO/IEC_JTC_1/SC_7" title="ISO/IEC JTC 1/SC 7">ISO/IEC standards</a></li>
<li><a href="ITIL" title="ITIL">ITIL</a></li>
<li><a href="Object_Management_Group" title="Object Management Group">OMG</a></li>
<li><a href="Project_Management_Body_of_Knowledge" title="Project Management Body of Knowledge">PMBOK</a></li>
<li><a href="Software_Engineering_Body_of_Knowledge" title="Software Engineering Body of Knowledge">SWEBOK</a></li></ul></div></div></td>
</tr><tr><td class="sidebar-content">
<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="color: var(--color-base)">Glossaries</div><div class="sidebar-list-content mw-collapsible-content hlist">
<ul><li><a href="Glossary_of_artificial_intelligence" title="Glossary of artificial intelligence">Artificial intelligence</a></li>
<li><a href="Glossary_of_computer_science" title="Glossary of computer science">Computer science</a></li>
<li><a href="Glossary_of_electrical_and_electronics_engineering" title="Glossary of electrical and electronics engineering">Electrical and electronics engineering</a></li></ul></div></div></td>
</tr><tr><td class="sidebar-content">
<div class="sidebar-list mw-collapsible mw-collapsed"><div class="sidebar-list-title" style="color: var(--color-base)">Outlines</div><div class="sidebar-list-content mw-collapsible-content hlist">
<ul><li><a href="Outline_of_software_development" title="Outline of software development">Outline of software development</a></li></ul></div></div></td>
</tr><tr><td class="sidebar-navbar"><style data-mw-deduplicate="TemplateStyles:r1239400231">
/* start https://en.wikipedia.org/ */
.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}
/* end https://en.wikipedia.org/ */
</style></td></tr></tbody></table>
<p>In <a href="Computer_science" title="Computer science">computer science</a>, <b>program analysis</b><sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> is the process of analyzing the behavior of computer programs regarding a property such as correctness, robustness, safety and liveness.
Program analysis focuses on two major areas: <a href="Program_optimization" title="Program optimization">program optimization</a> and <a href="Program_correctness" class="mw-redirect" title="Program correctness">program correctness</a>. The first focuses on improving the program’s performance while reducing the resource usage while the latter focuses on ensuring that the program does what it is supposed to do.
</p><p>Program analysis can be performed without executing the program (<a href="Static_program_analysis" title="Static program analysis">static program analysis</a>), during runtime (<a href="Dynamic_program_analysis" title="Dynamic program analysis">dynamic program analysis</a>) or in a combination of both.
</p>
<meta property="mw:PageProp/toc">
<div class="mw-heading mw-heading2"><h2 id="Static_program_analysis">Static program analysis</h2></div>
<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Static_program_analysis" title="Static program analysis">Static program analysis</a></div>
<p>In the context of program correctness, static analysis can discover vulnerabilities during the development phase of the program.<sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup> These vulnerabilities are easier to correct than the ones found during the testing phase since static analysis leads to the root of the vulnerability.
</p><p>Due to many forms of static analysis being computationally <a href="Undecidable_problem" title="Undecidable problem">undecidable</a>, the mechanisms for performing it may not always terminate with the correct answer. This can result in either <a href="False_positives_and_false_negatives" title="False positives and false negatives">false negatives</a> ("no problems found" when the code does in fact have issues) or <a href="False_positives_and_false_negatives" title="False positives and false negatives">false positives</a>, or because they may never return an incorrect answer but may also never terminate. Despite these limitations, static analysis can still be valuable: the first type of mechanism might reduce the number of vulnerabilities, while the second can sometimes provide strong assurance of the absence of certain classes of vulnerabilities.
</p><p>Incorrect optimizations are highly undesirable. So, in the context of program optimization, there are two main strategies to handle computationally undecidable analysis:
</p>
<ol><li>An optimizer that is expected to complete in a relatively short amount of time, such as the optimizer in an <a href="Optimizing_compiler" title="Optimizing compiler">optimizing compiler</a>, may use a truncated version of an analysis that is guaranteed to complete in a finite amount of time, and guaranteed to only find correct optimizations.</li>
<li>A third-party optimization tool may be implemented in such a way as to never produce an incorrect optimization, but also so that it can, in some situations, continue running indefinitely until it finds one (which may never happen). In this case, the developer using the tool would have to stop the tool and avoid running the tool on that piece of code again (or possibly modify the code to avoid tripping up the tool).</li></ol>
<p>However, there is also a third strategy that is sometimes applicable for languages that are not completely specified, such as <a href="C_(programming_language)" title="C (programming language)">C</a>. An optimizing compiler is at liberty to generate code that does anything at runtime – even crashes – if it encounters source code whose semantics are unspecified by the language standard in use.
</p>
<div class="mw-heading mw-heading3"><h3 id="Control-flow">Control-flow</h3></div>
<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Control-flow_analysis" title="Control-flow analysis">Control-flow analysis</a></div>
<p>The purpose of control-flow analysis is to obtain information about which functions can be called at various points during the execution of a program. The collected information is represented by a <a href="Control-flow_graph" title="Control-flow graph">control-flow graph</a> (CFG) where the nodes are instructions of the program and the edges represent the flow of control. By identifying code blocks and loops a CFG becomes a starting point for compiler-made optimizations.
</p>
<div class="mw-heading mw-heading3"><h3 id="Data-flow_analysis">Data-flow analysis</h3></div>
<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Data-flow_analysis" title="Data-flow analysis">Data-flow analysis</a></div>
<p>Data-flow analysis is a technique designed to gather information about the values at each point of the program and how they change over time. This technique is often used by compilers to optimize the code.
One of the most well known examples of data-flow analysis is <a href="Taint_checking" title="Taint checking">taint checking</a>, which consists of considering all variables that contain user-supplied data – which is considered "tainted", i.e. insecure – and preventing those variables from being used until they have been sanitized. This technique is often used to prevent <a href="SQL_injection" title="SQL injection">SQL injection</a> attacks. Taint checking can be done statically or dynamically.
</p>
<div class="mw-heading mw-heading3"><h3 id="Abstract_interpretation">Abstract interpretation</h3></div>
<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Abstract_interpretation" title="Abstract interpretation">Abstract interpretation</a></div>
<p>Abstract interpretation allows the extraction of information about a possible execution of a program without actually executing the program.
This information can be used by compilers to look for possible optimizations or for certifying a program against certain classes of bugs.
</p>
<div class="mw-heading mw-heading3"><h3 id="Type_systems">Type systems</h3></div>
<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Type_system" title="Type system">Type system</a></div>
<p>Type systems associate types to programs that fulfill certain requirements. Their purpose is to select a subset of programs of a language that are considered correct according to a property.
</p>
<ul><li><a href="Type_system#Type_checking" title="Type system">Type checking</a> – verify whether the program is accepted by the type system.</li></ul>
<p>Type checking is used in programming to limit how programming objects are used and what can they do. This is done by the compiler or <a href="Interpreter_(computing)" title="Interpreter (computing)">interpreter</a>. Type checking can also help prevent vulnerabilities by ensuring that a signed value isn't attributed to an unsigned variable.
Type checking can be done statically (at compile time), dynamically (at runtime) or a combination of both.
</p><p>Static type information (either <a href="Type_inference" title="Type inference">inferred</a>, or explicitly provided by type annotations in the source code) can also be used to do optimizations, such as replacing <a href="Boxed_type" class="mw-redirect" title="Boxed type">boxed arrays</a> with unboxed arrays.
</p>
<div class="mw-heading mw-heading3"><h3 id="Effect_systems">Effect systems</h3></div>
<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Effect_system" title="Effect system">Effect system</a></div>
<p>Effect systems are formal systems designed to represent the effects that executing a function or method can have. An effect codifies what is being done and with what it is being done – usually referred to as <i>effect kind</i> and <i>effect region</i>, respectively.
</p>
<div class="mw-heading mw-heading3"><h3 id="Model_checking">Model checking</h3></div>
<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Model_checking" title="Model checking">Model checking</a></div>
<p>Model checking refers to strict, formal, and automated ways to check if a <i>model</i> (which in this context means a formal model of a piece of code, though in other contexts it can be a model of a piece of hardware) complies with a given specification. Due to the inherent finite-state nature of code, and both the specification and the code being convertible into <a href="Logical_formula" class="mw-redirect" title="Logical formula">logical formulae</a>, it is possible to check if the system violates the specification using efficient algorithmic methods.
</p>
<div class="mw-heading mw-heading2"><h2 id="Dynamic_program_analysis">Dynamic program analysis</h2></div>
<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Dynamic_program_analysis" title="Dynamic program analysis">Dynamic program analysis</a></div>
<p>Dynamic analysis can use runtime knowledge of the program to increase the precision of the analysis, while also providing runtime protection, but it can only analyze a single execution of the problem and might degrade the program’s performance due to the runtime checks.
</p>
<div class="mw-heading mw-heading3"><h3 id="Testing">Testing</h3></div>
<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Software_testing" title="Software testing">Software testing</a></div>
<p>Software should be tested to ensure its quality and that it performs as it is supposed to in a reliable manner, and that it won’t create conflicts with other software that may function alongside it. The tests are performed by executing the program with an input and evaluating its behavior and the produced output.
Even if no security requirements are specified, additional <a href="Security_testing" title="Security testing">security testing</a> should be performed to ensure that an attacker can’t tamper with the software and steal information, disrupt the software’s normal operations, or use it as a pivot to attack its users.
</p>
<div class="mw-heading mw-heading3"><h3 id="Monitoring">Monitoring</h3></div>
<p>Program monitoring records and logs different kinds of information about the program such as resource usage, events, and interactions, so that it can be reviewed to find or pinpoint causes of abnormal behavior. Furthermore, it can be used to perform security audits. Automated monitoring of programs is sometimes referred to as <a href="Runtime_verification" title="Runtime verification">runtime verification</a>.
</p>
<div class="mw-heading mw-heading3"><h3 id="Program_slicing">Program slicing</h3></div>
<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Program_slicing" title="Program slicing">Program slicing</a></div>
<p>For a given subset of a program’s behavior, program slicing consists of reducing the program to the minimum form that still produces the selected behavior. The reduced program is called a “slice” and is a faithful representation of the original program within the domain of the specified behavior subset.
Generally, finding a slice is an unsolvable problem, but by specifying the target behavior subset by the values of a set of variables, it is possible to obtain approximate slices using a data-flow algorithm. These slices are usually used by developers during debugging to locate the source of errors.
</p>
<div class="mw-heading mw-heading2"><h2 id="See_also">See also</h2></div>
<ul><li><a href="Automated_code_review" title="Automated code review">Automated code review</a></li>
<li><a href="Language-based_security" title="Language-based security">Language-based security</a></li>
<li><a href="Polyvariance" title="Polyvariance">Polyvariance</a></li>
<li><a href="Profiling_(computer_programming)" title="Profiling (computer programming)">Profiling (computer programming)</a></li>
<li><a href="Program_verification" class="mw-redirect" title="Program verification">Program verification</a></li>
<li><a href="Termination_analysis" title="Termination analysis">Termination analysis</a></li></ul>
<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>
<style data-mw-deduplicate="TemplateStyles:r1239543626">
/* start https://en.wikipedia.org/ */
.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}
/* end https://en.wikipedia.org/ */
</style><div class="reflist">
<div class="mw-references-wrap"><ol class="references">
<li id="cite_note-1"><span class="mw-cite-backlink"><b><a href="#cite_ref-1">^</a></b></span> <span class="reference-text">Nielson, F., Nielson, H. R., & Hankin, C. (2015). <a rel="nofollow" class="external text" href="https://books.google.com/books?id=YseqCAAAQBAJ">Principles of program analysis</a>. Springer.</span>
</li>
<li id="cite_note-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-2">^</a></b></span> <span class="reference-text">Jovanovic, N., Kruegel, C., & Kirda, E. (2006, May). Pixy: A static analysis tool for detecting web application vulnerabilities. In Security and Privacy, 2006 IEEE Symposium on (pp. 6-pp). IEEE.</span>
</li>
</ol></div></div>
<div class="mw-heading mw-heading2"><h2 id="Further_reading">Further reading</h2></div>
<ul><li><style data-mw-deduplicate="TemplateStyles:r1238218222">
/* start https://en.wikipedia.org/ */
.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}
/* end https://en.wikipedia.org/ */
</style><cite id="CITEREFAgrawalHorgan" class="citation book cs1">Agrawal, Hiralal; Horgan, Joseph R. <a rel="nofollow" class="external text" href="https://www.cs.columbia.edu/~junfeng/08fa-e6998/sched/readings/slicing.pdf"><i>Dynamic program slicing</i></a> <span class="cs1-format">(PDF)</span>.</cite></li>
<li><cite id="CITEREFChunleiGangYiqi2009" class="citation book cs1">Chunlei, Wang; Gang, Zhao; Yiqi, Dai (2009). "An Efficient Control Flow Security Analysis Approach for Binary Executables". <i>2009 2nd IEEE International Conference on Computer Science and Information Technology</i>. pp. <span class="nowrap">272–</span>276. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FICCSIT.2009.5234950">10.1109/ICCSIT.2009.5234950</a>. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>978-1-4244-4519-6</bdi>. <a href="S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:10551500">10551500</a>.</cite></li>
<li><cite id="CITEREFNielsonNielsonHankin2005" class="citation book cs1">Nielson, Flemming; <a href="Hanne_Riis_Nielson" title="Hanne Riis Nielson">Nielson, Hanne Riis</a>; Hankin, Chris (2005). <i>Principles of Program Analysis</i>. <a href="Springer_Science%2BBusiness_Media" title="Springer Science+Business Media">Springer Science+Business Media</a>.</cite></li></ul>
<div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2></div>
<ul><li><span class="noviewer" typeof="mw:File"></span> Media related to <a href="https://commons.wikimedia.org/wiki/Category:Program_analysis" class="extiw external" title="commons:Category:Program analysis">Program analysis</a> at Wikimedia Commons</li></ul>
<div class="navbox-styles"><style data-mw-deduplicate="TemplateStyles:r1236075235">
/* start https://en.wikipedia.org/ */
.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}
/* end https://en.wikipedia.org/ */
</style></div><div role="navigation" class="navbox" aria-labelledby="Program_analysis496" style="padding:3px"><table class="nowraplinks hlist mw-collapsible expanded navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="3"><div id="Program_analysis496" style="font-size:114%;margin:0 4em"></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%;background:#e5e5ff;">Key<br>concepts</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Control-flow_graph" title="Control-flow graph">Control-flow graph</a></li>
<li><a href="Correctness_(computer_science)" title="Correctness (computer science)">Correctness</a></li>
<li><a href="Hyperproperty" title="Hyperproperty">Hyperproperties</a></li>
<li><a href="Invariant_(computer_science)" class="mw-redirect" title="Invariant (computer science)">Invariants</a></li>
<li><a href="Path_explosion" title="Path explosion">Path explosion</a></li>
<li><a href="Polyvariance" title="Polyvariance">Polyvariance</a></li>
<li><a href="Rice's_theorem" title="Rice's theorem">Rice's theorem</a></li>
<li><a href="Runtime_verification" title="Runtime verification">Runtime verification</a></li>
<li><a href="Safety_and_liveness_properties" title="Safety and liveness properties">Safety and liveness</a></li>
<li><a href="Undefined_behavior" title="Undefined behavior">Undefined behavior</a></li></ul>
</div></td><td class="noviewer navbox-image" rowspan="4" style="width:1px;padding:0 0 0 2px"><div><span typeof="mw:File"></span></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;background:#e5e5ff;"><a href="Semantics_(computer_science)" title="Semantics (computer science)">Semantics</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Types</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Axiomatic_semantics" title="Axiomatic semantics">Axiomatic</a></li>
<li><a href="Denotational_semantics" title="Denotational semantics">Denotational</a>
<ul><li><a href="Categorical_logic" title="Categorical logic">Categorical semantics</a></li></ul></li>
<li><a href="Operational_semantics" title="Operational semantics">Operational</a>
<ul><li><a href="Big_Step_Semantics" class="mw-redirect" title="Big Step Semantics">Big-step</a></li>
<li><a href="Small_Step_Semantics" class="mw-redirect" title="Small Step Semantics">Small-step</a></li></ul></li></ul>
</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Model_of_computation" title="Model of computation">Models</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Lambda_calculus" title="Lambda calculus">Lambda calculus</a></li>
<li><a href="Petri_net" title="Petri net">Petri net</a></li>
<li><a href="Process_calculus" title="Process calculus">Process calculus</a></li>
<li><a href="Abstract_rewriting_system" title="Abstract rewriting system">Rewriting system</a></li>
<li><a href="Finite-state_machine" title="Finite-state machine">State machine</a></li>
<li><a href="Turing_machine" title="Turing machine">Turing machine</a></li></ul>
</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;background:#e5e5ff;">Analyses</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Static_program_analysis" title="Static program analysis">Static</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Abstract_interpretation" title="Abstract interpretation">Abstract interpretation</a></li>
<li><a href="Alias_analysis" title="Alias analysis">Alias</a></li>
<li><a href="Control-flow_analysis" title="Control-flow analysis">Control flow</a>
<ul><li>kCFA</li></ul></li>
<li><a href="Data-flow_analysis" title="Data-flow analysis">Data-flow</a></li>
<li><a href="Dependence_analysis" title="Dependence analysis">Dependence</a></li>
<li><a href="Effect_system" title="Effect system">Effect system</a></li>
<li><a href="Escape_analysis" title="Escape analysis">Escape</a></li>
<li><a href="Model_checking" title="Model checking">Model checking</a></li>
<li><a href="Pointer_analysis" title="Pointer analysis">Pointer</a></li>
<li><a href="Shape_analysis_(program_analysis)" title="Shape analysis (program analysis)">Shape</a></li>
<li><a href="Symbolic_execution" title="Symbolic execution">Symbolic execution</a></li>
<li><a href="Termination_analysis" title="Termination analysis">Termination</a></li>
<li><a href="Type_system" title="Type system">Type systems</a></li>
<li><a href="Typestate_analysis" title="Typestate analysis">Typestate</a></li></ul>
</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Dynamic_program_analysis" title="Dynamic program analysis">Dynamic</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Dynamic_data-flow_analysis" class="mw-redirect" title="Dynamic data-flow analysis">Data-flow</a>
<ul><li>Taint tracking</li></ul></li>
<li><a href="Concolic_testing" title="Concolic testing">Concolic testing</a></li>
<li><a href="Fuzzing" title="Fuzzing">Fuzzing</a></li>
<li>Invariant inference</li>
<li><a href="Program_slicing" title="Program slicing">Program slicing</a></li>
<li><a href="Software_testing" title="Software testing">Testing</a></li></ul>
</div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;background:#e5e5ff;"><a href="Formal_methods" title="Formal methods">Formal<br>methods</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Concepts</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Curry%E2%80%93Howard_correspondence" title="Curry–Howard correspondence">Curry–Howard correspondence</a></li>
<li><a href="Loop_invariant" title="Loop invariant">Loop invariant</a></li>
<li><a href="Refinement_(computing)" title="Refinement (computing)">Refinement</a></li>
<li><a href="Side_effect_(computer_science)" title="Side effect (computer science)">Side effect</a></li>
<li><a href="Soundness" title="Soundness">Soundness</a> and <a href="Completeness_(logic)" title="Completeness (logic)">completeness</a></li>
<li><a href="Formal_specification" title="Formal specification">Specification</a>
<ul><li><a href="Specification_language" title="Specification language">Languages</a></li></ul></li>
<li><a href="Formal_verification" title="Formal verification">Verification</a></li></ul>
</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Logics</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Hoare_logic" title="Hoare logic">Hoare</a></li>
<li>Incorrectness</li>
<li><a href="Linear_logic" title="Linear logic">Linear</a></li>
<li><a href="Separation_logic" title="Separation logic">Separation</a></li>
<li><a href="Temporal_logic" title="Temporal logic">Temporal</a></li></ul>
</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Data_structure" title="Data structure">Data structures</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Binary_decision_diagram" title="Binary decision diagram">BDD</a></li>
<li><a href="E-graph" title="E-graph">E-graph</a></li>
<li><a href="Hash_consing" title="Hash consing">Hashcons</a></li>
<li><a href="Disjoint-set_data_structure" title="Disjoint-set data structure">Union-find</a></li></ul>
</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Tools</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Constraint_programming" title="Constraint programming">Constraint solvers</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Constrained_Horn_clauses" title="Constrained Horn clauses">CHC</a></li>
<li><a href="SAT_solver" title="SAT solver">SAT</a></li>
<li><a href="Satisfiability_modulo_theories" title="Satisfiability modulo theories">SMT</a></li></ul>
</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Formal_methods#Lightweight_formal_methods" title="Formal methods">Lightweight</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="Alloy_(specification_language)" title="Alloy (specification language)">Alloy</a></li>
<li><a href="TLA%2B" title="TLA+">TLA+</a></li></ul>
</div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="Proof_assistant" title="Proof assistant">Proof assistants</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em">
<ul><li><a href="ACL2" title="ACL2">ACL2</a></li>
<li><a href="Agda_(programming_language)" title="Agda (programming language)">Agda</a></li>
<li><a href="F*_(programming_language)" title="F* (programming language)">F*</a></li>
<li><a href="HOL_Light" title="HOL Light">HOL Light</a></li>
<li><a href="HOL_(proof_assistant)" title="HOL (proof assistant)">HOL4</a></li>
<li><a href="Idris_(programming_language)" title="Idris (programming language)">Idris</a></li>
<li><a href="Isabelle_(proof_assistant)" title="Isabelle (proof assistant)">Isabelle</a>
<ul><li><a href="Isabelle/HOL" class="mw-redirect" title="Isabelle/HOL">Isabelle/HOL</a></li></ul></li>
<li><a href="Lean_(proof_assistant)" title="Lean (proof assistant)">Lean</a></li>
<li><a href="LEGO_(proof_assistant)" title="LEGO (proof assistant)">LEGO</a></li>
<li><a href="Mizar_system" title="Mizar system">Mizar</a></li>
<li><a href="Nuprl" title="Nuprl">NuPRL</a></li>
<li><a href="Prototype_Verification_System" title="Prototype Verification System">PVS</a></li>
<li><a href="Rocq" title="Rocq">Rocq</a></li>
<li><a href="Twelf" title="Twelf">Twelf</a></li></ul>
</div></td></tr></tbody></table><div></div></td></tr></tbody></table><div></div></td></tr><tr><td class="navbox-abovebelow" colspan="3" style="font-weight:bold;"><div>
<ul><li><span class="noviewer" typeof="mw:File"><span title="Category"></span></span> Category</li>
<li><span class="noviewer" typeof="mw:File"><span title="List-Class article"></span></span> Outline</li>
<li><span class="noviewer" typeof="mw:File"><span title="List-Class article"></span></span> Glossary</li></ul>
</div></td></tr></tbody></table></div></div><!--htdig_noindex--><div><div class="zim-footer">
This article is issued from <a class="external text" title="Last edited on 2025-01-15" href="https://en.wikipedia.org/wiki/?title=Program_analysis&oldid=1269565085">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.
</div>
</div><!--/htdig_noindex--></div>
</div>
</main>
</div>
</div>
</div>
</body></html>